\chapter{Analysis}
Section \ref{sec:requirements} in the design chapter lists the requirements of
the separation kernel concept presented in this document. This chapter analyzes
how the Muen kernel implementation outlined in chapter \ref{chap:impl} meets
these requirements.

Section \ref{sec:separation} analyzes the separation properties of the kernel
while section \ref{sec:information-flow} discusses the flow of information
between subjects. The architecture support for the kernel as well as for
subjects is described in section \ref{sec:arch-support}. Section
\ref{sec:impl-assurance} examines the high robustness and assurance claims of
the Muen kernel implementation.

\section{Separation}\label{sec:separation}
The main requirement of a separation kernel is, as the name implies, to provide
strong separation of components to allow the construction of a trusted
high-assurance system. Section \ref{subsec:vmx-controls} analyzes how the VMX
configuration in the native and VM profiles ensures that subjects are not able
to widen their permissions by modifying execution environment values. Sections
\ref{subsec:system-resources} and \ref{subsec:exec-env-sep} examine how system
resources and the state of the execution environment are separated in detail.
The aspect of temporal isolation is explored separately in section
\ref{subsec:temp-isolation}.

Separation is not only important for subjects, but kernel resources must be
protected from unauthorized access as well. This aspect is also discussed in
this section.

\subsection{VMX Controls}\label{subsec:vmx-controls}
The instructions listed in Intel SDM \cite{IntelSDM}, volume 3A, section 25.1.2
cause a VM exit unconditionally when executed in VMX non-root mode, i.e. they
do not depend on VMX control settings in a subject VMCS. This section analyzes
instructions and events leading to a trap which depend on the settings of the
VM execution, entry and exit controls in the VMCS.

The VMX control settings are very restrictive to avoid side- or covert-channels.
Furthermore a subject must not be allowed to alter execution state which would
give access to resources not granted by policy.

Table \ref{tab:profiles-cond-vm-exits} shows the instructions and events which
conditionally lead to a VM exit depending on the VMX control settings of the
subject's profile. The configuration is very similar, except that VM subjects
are allowed to run their own memory management code, as described in the
following section \ref{subsubsec:control-regs}. Also, exceptions must be handled
by the operating system running in the VM subject profile. Only triple-faults
resulting from unhandled double-faults lead to a VM exit in this profile.

Access to I/O ports or MSRs\index{MSR} which are not granted by policy lead to a
VM exit for both profiles.

\begin{table}[h]
	\centering
	\begin{minipage}[c]{8cm}
	\begin{tabular}{l|c|c}
		\textbf{Event} & \textbf{Native} & \textbf{VM} \\
		\hline
		External interrupt   & \checkmark & \checkmark  \\
		VMX preemption timer & \checkmark & \checkmark  \\
		Execute \texttt{INVLPG}\footnote{Invalidate TLB Entry}
		& \checkmark & \checkmark \\
		Execute \texttt{MONITOR}\footnote{Set Up Monitor Address}
		& \checkmark & \checkmark \\
		Execute \texttt{MWAIT}\footnote{Monitor Wait}
		& \checkmark & \checkmark \\
		Execute \texttt{RDPMC}\footnote{Read Performance-Monitoring Counters}
		& \checkmark & \checkmark \\
		Execute \texttt{RDTSC}\footnote{Read Time-Stamp Counter}
		& \checkmark & \checkmark \\
		Execute \texttt{WBINVD}\footnote{Write Back and Invalidate Cache}
		& \checkmark & \checkmark \\
		MOV to CR3                  & \checkmark & \\
		MOV from CR3                & \checkmark & \\
		MOV to CR8                  & \checkmark & \checkmark \\
		MOV from CR8                & \checkmark & \checkmark \\
		MOV to/from debug registers & \checkmark & \checkmark \\
		\hline
		I/O port access & \checkmark & \checkmark \\
		MSR access      & \checkmark & \checkmark \\
		Exceptions      & \checkmark & \\
	\end{tabular}
	\end{minipage}
	\caption{Subject profile VM exit comparison}
	\label{tab:profiles-cond-vm-exits}
\end{table}

\subsection{System Resources}\label{subsec:system-resources}
System resources are assigned to subjects according to the system policy. The
kernel does not by itself perform policy decisions, but instead only applies
the linked in policy specifications and management data structures.

This means that the policy writer must make sure that the system specification
meets the requirements of a particular use-case.

\subsubsection{Memory}
Memory is assigned to the kernel and subjects by adding memory regions to the
appropriate specifications in the system policy. Memory assignment is therefore
static and cannot be changed at runtime.

If strict separation is desired, care must be taken that subject memory regions
do not overlap except for cases where a communication channel is explicitly
required. The same holds true for unintended overlaps of kernel and subject
memory.  While the policy compiler performs sanity checks, it does not currently
provide support to avoid unintended memory overlaps.

\subsubsection{Devices}
Devices are accessed using memory or port I/O. Interrupts are used to inform
subjects about device related incidents.

The assignment of a device to a subject automatically allows access to the
resources provided by this device. The policy compiler does not prohibit
assignment of one device to multiple subjects, as this could be a valid scenario
(e.g.  multiple subjects with the same trust level are allowed to access the VGA
console directly). Again, the policy writer must make sure that devices are
assigned correctly.

The kernel grants subject access to device resources as follows. Device access
via memory I/O is allowed to the subject by mapping the corresponding device
memory into the subject's address space. The page table for a subject containing
a mapping for device memory is generated automatically by the policy compiler
during system integration.

Port I/O is allowed using the VMCS I/O bitmap field. The correct bitmap is again
compiled by the system policy tool at integration time. The kernel simply assigns
the bitmap to the VMCS field during subject setup.

Device interrupts are routed to the correct subject as outlined in section
\ref{subsec:external-ints}.

\subsection{Execution Environment}\label{subsec:exec-env-sep}
Two mechanisms provide isolation of subject execution environments: saving and
restoring the architectural state or prohibiting access. An overview of the
state of a logical processor is given in section \ref{subsubsec:exec-env} and
specified in Intel SDM \cite{IntelSDM}, volume 1, section 3.2.1 and volume 3A,
section 8.7.1.

As mentioned in section \ref{sec:impl-subject}, parts of the execution
environment are saved and restored automatically by the VMX extensions on VM
entry or VM exit respectively, others must be handled manually. Table
\ref{tab:exec-env-storage} gives an overview about the different components and
the handling by VMX. Check marks in parenthesis indicate optional VMCS fields
which are only active when configured by the appropriate VMX control.
Components not handled by VMX must either be disallowed or saved manually to
prohibit unintended data flows.

The following subsections discuss each component of the execution environment in
detail.

\begin{table}[h]
	\centering
	\begin{tabular}{l|c}
		\textbf{Component} & \textbf{VMCS} \\
		\hline
		General purpose registers  & \\
		Segment registers          & \checkmark \\
		Instruction pointer        & \checkmark \\
		Flag register              & \checkmark \\
		CR0                        & \checkmark \\
		CR2                        & \\
		CR3                        & \checkmark \\
		CR4                        & \checkmark \\
		CR8                        & \\
		Descriptor table registers & \checkmark \\
		DR0-3                      & \\
		DR6                        & \\
		DR7                        & (\checkmark) \\
		x87 FPU registers          & \\
		MMX registers              & \\
		XMM registers              & \\
		MSRs                       & (\checkmark) \\
	\end{tabular}
	\caption{Execution environment and VMCS fields}
	\label{tab:exec-env-storage}
\end{table}

\subsubsection{General Purpose Registers}
General purpose registers (GPR\index{GPR}) are handled manually by the SPARK
CPU register type and the stack pointer field in the subject state record. See
section \ref{sec:impl-subject} for details about the structure of these two
records.  During initial subject setup, all GPR values are initialized to a
pristine state. The \texttt{Restore\_Registers} procedure implemented in the
kernel's \texttt{CPU} package restores the subject GPR values before a VM entry
by copying them to the correct processor registers using inline assembly.

On VM exit, the subject state in memory is reset to a pristine state. Then, the
VM exit reason is checked and if it is valid, the GPR values are copied from the
processor registers into the subject state. The kernel is halted on invalid exit
reasons, since this indicates a serious error condition.

\subsubsection{Segment Registers}
Segment registers are managed by VMX automatically inside the VMCS. The subject
VMCS both stores the visible segment selector\index{segment selector} as well as
the hidden part composed of the base address, segment limit, and access rights
values\footnote{The hidden part of a segment register is also called
\emph{descriptor cache} or \emph{shadow register}.} (see Intel SDM
\cite{IntelSDM}, volume 3A, section 3.4.3). The kernel initializes the segment
registers of a subject to the values shown by table \ref{tab:vmcs-segment-regs}.
The different values of the CS register is a result of the native subject code
being 64-bit, while the VM subject uses a 32-bit segment. For an explanation of
the access rights format see Intel SDM \cite{IntelSDM}, volume 3C,
section 24.4.1.

The segment registers FS and GS are disabled on subject setup by initializing
the VMCS access rights field for these registers to the value
\texttt{0x10000}\footnote{Unusable segment}.  A subject can enable them on
demand by loading an appropriate segment descriptor.

\begin{table}[h]
	\centering
	\begin{minipage}[c]{8cm}
	\begin{tabular}{l|c|c|c}
		\textbf{Register} & \textbf{Selector} & \textbf{Limit} & \textbf{AR} \\
		\hline
		CS & \texttt{0x08} & \texttt{0xffffffff} &
		\texttt{0xa09b}\footnote{Native subject profile} /
		 \texttt{0xc09b}\footnote{VM subject profile} \\
		DS & \texttt{0x10} & \texttt{0xffffffff} & \texttt{0x0c093} \\
		ES & \texttt{0x10} & \texttt{0xffffffff} & \texttt{0x0c093} \\
		FS & -             & -                   & \texttt{0x10000} \\
		GS & -             & -                   & \texttt{0x10000} \\
		SS & \texttt{0x10} & \texttt{0xffffffff} & \texttt{0x0c093} \\
		TR & \texttt{0x18} & \texttt{0x000000ff} & \texttt{0x0008b} \\
	\end{tabular}
	\end{minipage}
	\caption{VMCS segment register fields}
	\label{tab:vmcs-segment-regs}
\end{table}

Even though both subject profiles allow the modification of segment registers
and the associated descriptor tables, a subject is unable to access memory areas
not granted by policy. For native subjects, paging with a page table generated
from the policy is active and cannot be disabled (see the following section
\ref{subsubsec:control-regs} about control registers). Access to an illegal
memory region using a segment selector cannot bypass paging and results in a
page fault. VM subjects are constrained by the Intel EPT mechanism, where
access to disallowed memory results in an EPT violation trap.

\subsubsection{Instruction Pointer}
The instruction pointer is managed by VMX and initially set to the subject's
entry point. This value is read from the generated system policy.

Because it must be possible to modify the instruction pointer for emulation, it
is also copied to the in-memory subject state, which can be made accessible to a
subject monitor.

\subsubsection{Flag Register}
The flag register (EFLAGS in 32-bit mode, RFLAGS in 64-bit mode) is managed in
the VMCS region of the subject and set to the initial value 2 (only the reserved
bit 1 is set, all other bits are cleared).

\subsubsection{Control Registers}\label{subsubsec:control-regs}
Control registers CR0 and CR4 are managed by VMX automatically and initialized
to the values shown by table \ref{tab:vmcs-control-regs}. These values depend
on the subject profile.

\begin{table}[h]
	\centering
	\begin{tabular}{l|c|c}
		\textbf{Register} & \textbf{Native} & \textbf{VM} \\
		\hline
		CR0 & \texttt{0x80010035} & \texttt{0x00000035} \\
		CR0 bitmask & \texttt{0xffffffff} & \texttt{0x7ffeffff} \\
		CR4 & \texttt{0x00002020} & \texttt{0x00002000} \\
		CR4 bitmask & \texttt{0xffffffff} & \texttt{0xffffffef} \\
	\end{tabular}
	\caption{VMCS control register fields}
	\label{tab:vmcs-control-regs}
\end{table}

Since a VM subject is started in protected mode with paging disabled, bits 16
and 31 of CR0 are cleared, whereas they are set in the native profile. The CR0
mask field in the VMCS allows the VM subject to modify these two bits (bitmask
value \texttt{0x7ffeffff}) to enable paging without causing a VM exit. On the
other hand, the bitmask value of \texttt{0xffffffff} disallows modification of
any bit in CR0 for native subjects, paging is already enabled by default and
cannot be disabled. The remaining bits are identical. Bit 0 indicates protected
mode and bit 2 disables the x87 FPU for subjects. Bit 4 is reserved and must be
set for both profiles. Bit 5 enables native FPU error reporting (see table 9-3
in \cite{IntelSDM}, volume 3A, section 9.2.2).

Bit 13 (VMXE) in the CR4 control register is set for both profiles. This bit is
a prerequisite for VMX operation not only for the host but also for the guest
state. Bit 5 (Physical Address Extension, PAE\index{PAE}) in the native profile
is a prerequisite for IA-32e mode. While modifications of CR4 in a native
subject lead to a trap, the VM profile allows the modification of bit 4 (Page
Size Extensions, PSE\index{PSE}). This allows 4 MB pages in 32-bit paging mode
(used for example by the xv6 OS\index{OS}).

CR3 is also managed by VMX. Again, the handling depends on the subject profile.
Native subjects are not allowed to change the value of CR3 since it points to
the generated page table which confines the usable memory of a subject. The
native subject profile enables both load and store VM exit controls for CR3,
resulting in a trap if a native subject tries to tamper with the CR3 value
(section \ref{subsec:vmx-controls} and Intel SDM \cite{IntelSDM}, volume 3C,
section 24.6.2). VM subjects are allowed to run their own memory management
code within the boundaries set by the Intel EPT mechanism, see section
\ref{subsubsec:ept}. A value moved into the CR3 control register is treated as
a guest-physical address and the instruction does not cause a VM exit.

CR2 is not managed by VMX but copied manually from the subject state to the
processor register and back. The initial value of CR2 is zero. Accessing
control register CR8 leads to a trap for both profiles. For more information
about the meaning of control register bits, see Intel SDM \cite{IntelSDM},
volume 3C, section 2.5.

\subsubsection{Descriptor Table Registers}
Both subject profiles allow the management of the Global Descriptor Table
(GDT\index{GDT}) and the Interrupt Descriptor Table (IDT\index{IDT}). The GDTR
and IDTR registers are stored in the guest-state area in the VMCS and updated
automatically.

The Local Descriptor Table Register (LDTR\index{LDTR}) is disabled by setting
the corresponding access rights field in the VMCS to the value \texttt{0x10000}.
It can be enabled by subjects if needed. The LDTR register is also managed by
VMX automatically.

\subsubsection{Debug Registers}
Debug registers are not handled by VMX and the kernel does not currently store
them in the subject state. Instead, access is disallowed by setting the "MOV-DR
exiting" VMX processor control (Intel SDM \cite{IntelSDM}, volume 3C, section
24.6.2) in both subject profiles. This leads to a trap when trying to move data
into or from debug registers.

\subsubsection{x87 FPU Registers}
The x87 FPU state is not handled by VMX. Currently, execution of a x87 FPU
instruction generates a device-not-available exception (\#NM). This is due to
the CR0.EM bit set in the subject control register (see Intel SDM, volume 3A,
sections 2.5 and 9.2).

Enabling the FPU would require the kernel to manage the complete FPU state of
the processor. This is currently not implemented but the usage of the
\texttt{XSAVE}, \texttt{XRSTOR} instructions and the appropriate configuration
of the XCR0 register could be used to support x87 instructions for subjects.

According to table 2-2 in \cite{IntelSDM}, volume 3A, section 2.5, the
\texttt{WAIT}/\texttt{FWAIT} instruction does still execute even with the CR0.EM
bit set. This is not considered problematic because the instruction is only used
to wait for pending floating-point exceptions.

\subsubsection{MMX Registers}
The MMX state is not handled by VMX and, similar to the x87 FPU state, the
kernel does not save its state manually. MMX instructions currently lead to a
\#UD exception because the CR0.EM bit is set in the VMCS guest-state field
(Intel SDM \cite{IntelSDM}, volume 3A, section 12.1).

\subsubsection{XMM Registers}
The Streaming SIMD\index{SIMD}\footnote{Single instruction, multiple data}
Extensions (SSE\index{SSE}) provide an extended processor state with sixteen
additional XMM registers and one MXCSR register. The \texttt{XSAVE},
\texttt{XRSTOR} instructions are provided for operating systems to save and
restore processor state extensions according the configuration in the XCR0
register. All SSE\footnote{SSE, SSE2, SSE3, SSSE3 and SSE4} extensions share
the same state and experience the identical set of numerical exception behavior.

The XCR0\index{XCR0}\footnote{XFEATURE\_ENABLED\_MASK register} is read with
\texttt{XGETBV} and written with the \texttt{XSETBV} instruction. The
modification of the XCR0 register with \texttt{XSETBV} from within VMX non-root
mode causes a VM exit unconditionally, see Intel SDM \cite{IntelSDM}, volume
3C, section 25.1.2.

If an SSE/SSE2/SSE3/SSSE3/SSE4 instruction is executed by a subject, an invalid
opcode exception (\#UD) is generated and a trap occurs (see Intel SDM
\cite{IntelSDM}, volume 3A, section 13.2). This is again due to the CR0.EM bit
set for subjects.

SSE/SSE2/SSE3/SSSE3/SSE4 instructions not affected by the EM flag include
(\cite{IntelSDM}, 2.5):
\begin{itemize}
	\item PAUSE (\emph{Spin Loop Hint})
	\item PREFETCHh (\emph{Prefetch Data Into Caches})
	\item SFENCE, LFENCE, MFENCE (\emph{Used for memory ordering})
	\item MOVNTI (\emph{Store Doubleword Using Non-Temporal Hint})
	\item CLFLUSH (\emph{Flush Cache Line})
	\item CRC32 (\emph{Accumulate CRC32 Value})
	\item POPCNT (\emph{Return the Count of Number of Bits Set to 1})
\end{itemize}

Even though these instructions are provided by a SSE instruction set, they do
not interact with the x87 FPU or extended processor states and are therefore
considered uncritical.

The Intel Advanced Vector Extensions (AVX\index{AVX}) increase the width of the
SIMD registers from 128 bits to 256 bits and rename them from XMM0-XMM15 to
YMM0-YMM15 (in IA-32e mode). In processors with AVX support, the legacy SSE
instructions (which previously operated on 128-bit XMM registers) now operate on
the lower 128 bits of the YMM registers. Execution of an AVX instruction leads
to a \#UD exception because of the enabled CR0.EM bit.

\subsubsection{Model-specific Registers (MSRs)}
Direct access to MSRs from subjects is allowed if granted by policy. Access can
be read-only, write-only or read-write. The writer of the system policy must
take care not to allow unintended access to MSRs.

The VMCS MSR bitmap which governs access to MSRs is generated from the policy by
the policy compiler. The kernel initializes the VMCS MSR bitmap field during
subject setup using the generated bitmap.

\subsection{Temporal Isolation}\label{subsec:temp-isolation}
The Muen kernel scheduler executes subjects according to a scheduling plan
specified in the system policy. The scheduling plans have a fixed cyclic
structure and are divided into major frames that are comprised of a number of
minor frames. The \texttt{skpolicy} tool guarantees that the sum of all minor
frame lengths per logical CPU for a given major frame are of equal length.

To keep multicore systems in sync and avoid drift between the schedulers of
kernels running on different cores, a global barrier is employed. At the
beginning of a new major frame, all cores synchronize on the barrier. Once all
cores are ready, the barrier is released and simultaneous execution of the
first minor frame starts.

Strict adherence to a given plan is implemented using the VMX preemption timer.
Subjects are executed for the time slice mandated by the currently active minor
frame. If for some reason the timer is not deemed to be precise enough for a
particular use case, additional timer sources could be used to provide even
higher timer resolution and thus scheduling accuracy.

\section{Information Flow}\label{sec:information-flow}
This section reviews the mechanisms provided by the Muen kernel to enable
information flow between subjects.

\subsection{Shared Memory}
Shared memory is the main method for subjects to share information. Such regions
must be defined in the subject specification as part of the system policy. Use of
access attributes enables the definition of directed flows, where data can only
be transferred from source to destination.

The memory layout is fixed at integration time and the \texttt{skpolicy} tool
generates static page tables, which control the physically accessible memory of
each subject. These page tables are packaged into the final system image. As
long as the physical memory where paging structures reside, is not accessible,
they cannot be altered or changed at runtime. It is the policy writer's duty to
avoid mapping of any paging structures into the memory layout of subjects.

When running a subject, the kernel installs the corresponding paging structure
which instructs the processor's MMU to enforce the subject's address space
according to the policy. This guarantees that shared memory regions, as well as
all other memory resources for that matter, are only present if they are
explicitly specified.

\subsection{Events}
A second mechanism how information can flow from one subject to another is the
use of events. A subject can trigger an event, which ultimately leads to the
injection of an interrupt into a specific subject or a subject handover.

As with shared memory regions, events are defined as part of the subject
specification and consist of the event number, destination subject ID and
destination interrupt vector. All events that a subject can trigger must be
provided in the system policy.

A subject has to specify the number of the event it wants to trigger. The
subject basically selects one of the predefined events. If a malicious subject
passes an invalid event number, the kernel ignores the request. Thus only events
that are specified in the policy are valid and can be triggered.

\subsection{Traps}
The subject specification contains a trap table that specifies how each trap
should be handled. A trap table entry specifies a destination subject to which
the kernel should hand over execution, if the source subject causes a VM exit
with the given reason. If no entry for a given trap exists or if the trap is not
in the range of valid exit reasons, the kernel and thus the CPU executing that
subject is halted by invoking the kernel's panic handler. A future extension of
the kernel must improve the handling of invalid traps, e.g. by allowing to
stop or restart a subject which causes such a trap.

The traps that are reserved for internal kernel use cannot be specified in the
policy and take precedence over the subject trap table.

Since subject trap tables are part of the policy generated static information,
they cannot change at runtime. This ensures that traps are handled according to
policy and any unexpected trap will cause the kernel to panic and halt
execution.

\section{Architecture Support}\label{sec:arch-support}
This section reviews the hardware platforms the kernel is able to run on, as
well as the architectures the kernel provides to subjects as execution
environment.

The kernel allows the use of all available physical memory, since it does not
add any restrictions to memory management. Thus all properties of the Intel
IA-32e mode and 64-bit paging are preserved. This is also true for page
attribute tables (PAT), which control caching behavior. PAT is supported via the
system policy by the ability to specify the memory type of memory regions.

\subsection{Kernel}
As described in section \ref{subsec:init}, the kernel switches the processor to
the IA-32e mode during system initialization. It executes in 64-bit protected
mode with paging enabled.

The kernel uses advanced Intel VT-x virtualization features, which are shown in
the following list:

\begin{itemize}
	\item VMX preemption timer
	\item EPT
	\item Unrestricted guests
\end{itemize}

Since the kernel uses x2APIC to manage the CPU's local APIC, that feature must
also be present in the processor.

As a consequence, the kernel requires a fairly recent 64-bit Intel processor of
the \emph{Ivy Bridge} generation or newer. Even though AMD provides comparable
hardware virtualization features, the kernel is not compatible with such
processors. Adding support for multiple hardware virtualization extensions is
possible but would significantly increase implementation effort and, more
importantly, kernel complexity.

The following list summarizes the kernel memory usage:

\begin{itemize}
	\item AP trampoline [4 KB]
	\item VMXON region [4 KB per CPU]
	\item VMCS region [4 KB per subject]
	\item Kernel page tables [16 KB per CPU]
	\item Kernel code \& data [36 KB]
	\item Kernel per-CPU data  [4 KB per CPU]
	\item Kernel per-CPU stack [4 KB per CPU]
\end{itemize}

Except for the AP trampoline, which is fixed at physical address 0x0, the
location of all remaining memory regions can be controlled by the system policy.
Additional memory is necessary depending on the number of subjects and their
memory demands.

The hardware requirements can be met by any recent
COTS\footnote{Commercial off-the-shelf} x86 hardware based on an Ivy Bridge
Intel CPU, be it notebooks, workstations or server systems. It might be noted
that with the advent of new Intel-based tablets that are powered by VT-x capable
latest-gen Haswell processors, the Muen kernel should even be able to run on
mobile devices.

\subsection{Subject}
Subjects that make use of the native profile must be compiled and statically
linked 64-bit x86 binaries. They are executed by the kernel in IA-32e protected
mode with paging enabled. Write access to the CR3 control register is disallowed
which means native subjects have a static address space and are not allowed to
manage their memory via the MMU.

VM subjects start in 32-bit unpaged mode and are free to enable paging. They can
install their own paging structures and have full access to the CR3 control
register. EPT is used to confine VM subjects to the policy assigned memory. This
means that while VM subjects can perform their own memory management, the
address space is guaranteed to be static, which is identical to the native
profile.

Additionally, VM subjects are expected to perform exception handling by
installing an interrupt descriptor table. If a subject raises an exception, it
is vectored through the subject's IDT. Only a triple fault will cause a trap,
that the kernel will process as usual.

\section{Implementation Assurance}\label{sec:impl-assurance}
This section summarizes the properties of the Muen kernel that make a compelling
case to back up the high robustness and assurance claim of the implementation.

\subsection{Lean Implementation}
The implementation of the kernel has been reduced to essential functionality.
All mechanisms that are not strictly required to be part of the kernel have been
delegated to other components of the system, such as the policy compilation
tool.

A lot of responsibility rests with the correct policy specification, which is
the duty of the system integrator. The \texttt{skpolicy} tool transforms the
policy into static data, that the kernel then uses to enforce the policy without
having to understand the meaning of the compiled information. The kernel can
thus be regarded as a policy enforcement engine.

The emphasis put on use of advanced hardware features further reduces the scope
of functionality implemented in software. A good example is memory management,
where the kernel's sole responsibility is to provide the pre-generated page
tables to the MMU, which in turn enforces the memory layout specified by the
policy.

\subsection{Small Size}
The kernel including the small zero-footprint runtime has a low
SLOC\footnote{Source lines of code} count. The following list gives the source
code statistics generated with the \texttt{sloccount}
tool\footnote{\url{http://www.dwheeler.com/sloccount/}}, version 2.26:

\begin{itemize}
	\item 256 lines of Assembly
	\item 2463 lines of SPARK
\end{itemize}

Debugging code is not included, since all such lines\footnote{Currently spanning
over 123 lines} are wrapped in \texttt{pragma Debug} statements. The compiler
skips these parts of the source code completely, when building the kernel with
debugging disabled. Thus they are not included in the final release image of the
Muen kernel.

Policy-generated files are also omitted since they are static data structures
containing system specification information, which is not considered part of the
kernel. They are a transformed view of the policy accessible to the kernel.

The numbers show that the Muen kernel implementation is quite small, considering
the fact that the Ada/SPARK language favors readability of the code over
compactness. The size of the project allows for a complete review of the TCB
with moderate effort.

\subsection{Choice of Programming Language}
The vast majority of the kernel has been implemented using the SPARK language,
which is very well suited for the construction of high integrity systems.

System initialization is performed in assembly. Necessary CPU instructions,
e.g. to execute VT-x specific operations, are implemented as inline assembly
and made accessibly to SPARK via the SK.CPU package. The assembly code was
kept to the necessary minimum.

The rest of the kernel is written in SPARK. The major benefits of the
programming language are presented in section \ref{sec:spark}. The kernel is
clearly structured using packages which increases the readability of the code.
Paired with the small size, it is well suited for manual or automated review.

Using the SPARK tools, full absence of runtime errors has been proven. Table
\ref{tab:kernel-proof-sum} shows the proof summary generated by the SPARK tools,
as part of the build process.

\begin{table}[h]
	\centering
	\begin{tabular}{l c c c}
		& \textbf{Examiner} & \textbf{Simplifier} & \textbf{Total} \\
		Assert/Post    & 133 & 48  & 181 \\
		Precondition   & 0   & 9   & 9   \\
		Runtime check  & 0   & 432 & 432 \\
		Refinement VCs & 43  & 1   & 44 \\
		\hline
		\textbf{Total} & 176 & 490 & 666 \\
	\end{tabular}
	\caption{SPARK kernel proof summary}
	\label{tab:kernel-proof-sum}
\end{table}

A total of 666 verification conditions are generated, which have all been
discharged and thus proven correct. This means that all the SPARK code of the
Muen kernel is free from runtime errors and will not raise an exception.
Section \ref{sec:spark} lists all types of errors whose absence is proven. In
addition some functional properties were stated as postconditions and proven.

\subsection{Tools}
All supporting tools have been developed in Ada following a strict test-driven
development process. Each tool implementation is accompanied by a comprehensive
test suite which provides wide code coverage. The tools are released as part of
the Muen project under the GNU General Public License\index{GPL}.

\subsection{Verifiability}
The complete source code and documentation of this project are published online
at \url{http://muen.sk/}. Anybody can download all artifacts and perform a
manual review of the design and code.

Perhaps even more important is the fact that SPARK annotations are distributed
as part of the source code. Combined with the free availability of the GNAT Ada
compiler as well as the SPARK tools, this makes it possible to independently
reproduce the proof of absence of runtime errors and verify the claims made in
this document.

Verification of the TCB is tightly integrated into the automated build process.
Given the correct installation of all necessary tools, building and verifying
the Muen kernel is as simple as invoking the \texttt{make} command.

The small size of the code base should make it suitable for further analysis, be
it manual or automated. Having such a small kernel should lower the time and
effort needed for full formal verification, even though such a task is still
expected to be a substantial amount of work.
